n, i:. (i < n)  (i  upto(n)) 

latex

Definitions	x:A. B(x), P  Q, (x  l), {i..j}, x:A. B(x), A c B, t  T, A  B, i  j < k, P & Q, , A, False,
Lemmas	length upto, select upto, le wf, length wf1, int seg wf, upto wf, select wf, nat wf